using System;
using System.Threading;
using System.IO;
using System.Collections.Generic;
using System.Collections;

public class DeductiveMain
{
	static string stateFile = "../../state-forall.txt";
	//static string stateFile = "../../state.txt";
	//static string stateFile = "../../stateMin.txt";

	public static void deductiveLearning(){
		parseLispExpression();
	}
	
	
	
	static RewritesBase findRewrites(Node parseRes){
		RewritesBase rbase = new RewritesBase();
		List<Node> eqRules = findTop(parseRes,"=");
		foreach(Node r in eqRules){
			rbase.add(r);
		}
		return rbase;
	}
	
	
	
	static void parseLispExpression(){
	    Parser p = new Parser();
		StreamReader streamReader = new StreamReader(stateFile);
		string text = streamReader.ReadToEnd();
		streamReader.Close();
	
		Node parseRes = (Node)p.parse (text);
		Console.WriteLine("parseRes: "+parseRes);
		//new NodeWriter(Console.Out).write(parseRes);
		Console.Out.WriteLine();
		Console.WriteLine("Finished : "+text);
		
		List<Node> quests = findTop(parseRes, new string[]{"?","?solve"});
		//quests.AddRange(findTop(parseRes,"?solve"));
		
		RewritesBase rewrBase = findRewrites(parseRes);
		
		//NodeWriter wrt = new NodeWriter(Console.Out);
		foreach( Node quest in quests ){
			//Node cond = quest.childNode(0);
			Node q = quest.childNode(0);
			Console.WriteLine();
			//Console.Write("Quest compl="+Deductive.complexity(q)+" ");
			Console.WriteLine("Quest "+Node.nodeString(q));
			
			Deductive deduct = new Deductive(rewrBase);
			StateHist better = deduct.simplify(quest.Name.Equals("?solve"), /*cond,*/ q);
			if( better!=null ){
			  Console.WriteLine("Final result="+better.fullHistory());
			}
		}
	}
	

	static List<Node> findTop(Node n, string name){
		var ret = new List<Node>();
		foreach(Node nch in n.Children){
			if( nch.Name.Equals(name) ){
				ret.Add(nch);
			}
		}
		return ret;
	}

	static List<Node> findTop(Node n, string[] names){
		var ret = new List<Node>();
		foreach(Node nch in n.Children){
			foreach(var name in names){
				if( nch.Name.Equals(name) ){
					ret.Add(nch);
					break;
				}
			}
		}
		return ret;
	}

}

